Inference at * 1 
Iof proof for Lemma pi2 wf:



1. A : Type
2. B : AType
3. p : a:A  B(a)
  (p.2)  B(p.1) 

latex

 by ((D 3) 
CollapseTHEN (RWH pi1_evalC 0)) 

latex

C1: 

C1: 3. a : A
C1: 4. p1 : B(a)
C1:   (<a, p1>.2)  B(a)
C.

Definitions

t.1